$\forall$${\it es}$:ES, $R$:(E$\rightarrow$E$\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$x$, $y$:E. ($R$($x$,$y$)) $\Rightarrow$ ($x$ $<$ $y$)) $\Rightarrow$ ($\forall$$x$, $y$:E. Dec($R$($x$,$y$))) $\Rightarrow$ ($\forall$$y$, $x$:E. Dec($R$\^{}+($x$,$y$)))